#pragma once
#include "TermVariable.h"
#include "../Types/ArrowType.h"

using namespace std;


// ApplicationTerm command target

class ApplicationTerm : public Term
{

protected:
	TokenPair LeftRight;
	
public:	 
	virtual Token::const_reference getRight() const;
	virtual Term::const_reference getLeft() const;

public:
	bool isApplicationTerm() const{return true;};
	virtual bool isRedex() const;

public:
	ApplicationTerm(Term::const_reference, Token::const_reference, const string& ="");
	ApplicationTerm(const ApplicationTerm&);
	virtual ~ApplicationTerm();

public:   	
	//Token Overides
	Term::pointer normalized() const;
	Token::pointer applyArgument(Token::const_reference)  const;
	Token::pointer clone() const;
	bool isReducible() const;
	string toString() const;
	string view() const;
	bool operator==(Token::const_reference To) const;
	Token::pointer replaceAll(Token::const_reference, Token::const_reference) const;
	size_t complexity() const {return getLeft().complexity()+getRight().complexity()+Term::complexity();};

public:
	bool TypeOccursinFreeVariable(Type::const_reference Ty) const;
};

class InvertedListTerm : public	Term{
		
public:
//	bool isApplicationTerm() const{return true;};

protected:
	/************************
		((((0,1),2),3),4)
	************************/
	TokenVector  Applications;

public:	 
	Token::const_reference getRight() const;

public:
	InvertedListTerm(vector<Token*>, const string& ="");
	InvertedListTerm(Term::const_reference);
	InvertedListTerm(const InvertedListTerm&);
	virtual ~InvertedListTerm();

};

class VirtualInvertedListTerm : public	Term{
	
	/************************
		((((0,1),2),3),4)
	************************/
protected:
	vector<const Token*>  Applications;

public:
	bool isVirtualInvertedListTerm( ) const{return true;};
	Token::pointer toNewTerm(size_t, size_t=0) const;
	
public:
	Term::pointer normalized() const;
	Token::pointer applyArgument(Token::const_reference)  const;
	Token::pointer clone() const;
	bool isReducible() const;
	string toString() const;
	string view() const;
	bool operator==(Token::const_reference To) const;
	Token::pointer replaceAll(Token::const_reference, Token::const_reference) const;
	size_t complexity() const;
	bool TypeOccursinFreeVariable(Type::const_reference Ty) const;

public:
	Token::const_reference operator[ ](size_t ) const;
	void replaceElts(const VirtualInvertedListTerm&, size_t, size_t num=1);
	void push_back(Token::const_reference);
	size_t size( ) const {return Applications.size( );};

public:
	VirtualInvertedListTerm(Term::const_reference,  const string& ="");
	VirtualInvertedListTerm(const VirtualInvertedListTerm&);
	virtual ~VirtualInvertedListTerm( );

};






